Inference at * 1 3 1 0 2 1 3 
Iof proof for Lemma fincr wf:

.....wf..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. 
4. i : 
  (0  i)  Type 

latex

 by ((MemEqCD) 
CollapseTHEN (MemEqCD)) 

latex

C.

Definitions	, f(a), a < b, P  Q, , x:AB(x), Type, A  B, s = t, #$n, x:A. B(x), , t  T
Lemmas	le wf